package controller.sequentParser;

import java.io.Reader;

import model.ParseError;
import model.sequent.SequentToken;
import model.sequent.tokens.Atom;
import model.sequent.tokens.BiOperatorExpression;
import model.sequent.tokens.Expression;
import model.sequent.tokens.Sequent;
import model.sequent.tokens.SimpleOperatorExpression;

/**
 * Tail recursive parser for parsing input data to a Sequent tree.
 * 
 * @author Sjaak Smetsers (number?)
 * @author Karen Berntsen (s0815799)
 * @author Erik Stens (s0615374)
 */
public class SequentTRparser {
	private SequentTokenizer	tokens;
	
	public SequentTRparser(Reader input) throws ParseError {
		tokens = new SequentTokenizer(input);
	}
	
	public Sequent parse() throws ParseError {
		Sequent sequent = parseSequent();
		if (tokens.currentToken() == SequentToken.EOF) {
			return sequent;
		} else {
			throw new ParseError("End of input expected", tokens.currentToken().toString());
		}
	}
	
	/**
	 * Checks whether the next token is an operator.
	 **/
	public boolean parseOp(SequentToken operator) throws ParseError {
		if (tokens.currentToken() == operator) {
			tokens.nextToken();
			return true;
		}
		return false;
	}
	
	/**
	 * Creates a Sequent and adds true expressions and false expressions to it.
	 * 
	 * @return a Sequent tree
	 * @throws ParseError
	 */
	public Sequent parseSequent() throws ParseError {
		Sequent sequent = new Sequent();
		
		do {
			sequent.addTrueExpression(parseExpression());
		} while (parseOp(SequentToken.COMMA));
		
		if (parseOp(SequentToken.SEQUENT)) {
			do {
				sequent.addFalseExpression(parseExpression());
			} while (parseOp(SequentToken.COMMA));
			
			return sequent;
		} else {
			throw new ParseError("Sequent separator '@' or binary operator expected", tokens.currentToken().toString());
		}
	}
	
	// the following methods are based on our grammar (see /documents/grammar.docx)
	
	public Expression parseExpression() throws ParseError {
		Expression implicate = parseImplicate();
		for (boolean operator = parseOp(SequentToken.BI_IMPLICATE); operator; operator = parseOp(SequentToken.BI_IMPLICATE)) {
			implicate = new BiOperatorExpression(implicate, parseImplicate(), SequentToken.BI_IMPLICATE);
		}
		return implicate;
	}
	
	public Expression parseImplicate() throws ParseError {
		Expression or = parseOr();
		for (boolean operator = parseOp(SequentToken.IMPLICATE); operator; operator = parseOp(SequentToken.IMPLICATE)) {
			or = new BiOperatorExpression(or, parseOr(), SequentToken.IMPLICATE);
		}
		return or;
	}
	
	public Expression parseOr() throws ParseError {
		Expression and = parseAnd();
		for (boolean operator = parseOp(SequentToken.OR); operator; operator = parseOp(SequentToken.OR)) {
			and = new BiOperatorExpression(and, parseAnd(), SequentToken.OR);
		}
		return and;
	}
	
	public Expression parseAnd() throws ParseError {
		Expression not = parseNot();
		for (boolean operator = parseOp(SequentToken.AND); operator; operator = parseOp(SequentToken.AND)) {
			not = new BiOperatorExpression(not, parseNot(), SequentToken.AND);
		}
		return not;
	}
	
	public Expression parseNot() throws ParseError {
		if (parseOp(SequentToken.NOT)) {
			return new SimpleOperatorExpression(parseNot(), SequentToken.NOT);
		} else {
			return parseAtom();
		}
	}
	
	public Expression parseAtom() throws ParseError {
		switch (tokens.currentToken()) {
			case ATOM: {
				Atom atom = new Atom(tokens.getAtomName());
				tokens.nextToken();
				return atom;
			}
			case BRACKET_OPEN:
				tokens.nextToken();
				Expression expression = parseExpression();
				if (tokens.currentToken() == SequentToken.BRACKET_CLOSE) {
					tokens.nextToken();
					return expression;
				} else {
					throw new ParseError("Close bracket expected", tokens.currentToken().toString());
				}
			default:
				throw new ParseError("Atom expected", tokens.currentToken().toString());
		}
	}
}
